\begin{tabbing}
EO\=rderAxioms\{i\}($E$;\+
\\[0ex]${\it pred?}$;
\\[0ex]${\it info}$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(\=$\forall$$e$:$E$, $l$:IdLnk.\+\+
\\[0ex]$\exists$${\it e'}$:$E$.
\\[0ex]$\forall$${\it e''}$:$E$.
\\[0ex]rcv?(${\it info}$;${\it e''}$)
\\[0ex]$\Rightarrow$ sender(${\it info}$;${\it e''}$) $=$ $e$ $\in$ $E$
\\[0ex]$\Rightarrow$ link(${\it info}$;${\it e''}$) $=$ $l$ $\in$ IdLnk
\\[0ex]$\Rightarrow$ ${\it e''}$ $=$ ${\it e'}$ $\in$ $E$ $\vee$ cless($E$;${\it pred?}$;${\it info}$;${\it e''}$;${\it e'}$) \& loc(${\it info}$;${\it e'}$) $=$ destination($l$) $\in$ Id)
\-\\[0ex]\& (\=$\forall$$e$:$E$, ${\it e'}$:$E$.\+
\\[0ex]loc(${\it info}$;$e$) $=$ loc(${\it info}$;${\it e'}$) $\in$ Id $\Rightarrow$ ${\it pred?}$($e$) $=$ ${\it pred?}$(${\it e'}$) $\in$ $E$+Unit $\Rightarrow$ $e$ $=$ ${\it e'}$ $\in$ $E$)
\-\\[0ex]\& strongwellfounded($E$; $e$,${\it e'}$.pred!($E$;${\it pred?}$;${\it info}$;$e$;${\it e'}$))
\\[0ex]\& ($\forall$$e$:$E$. $\neg$first(${\it pred?}$;$e$) $\Rightarrow$ loc(${\it info}$;pred(${\it pred?}$;$e$)) $=$ loc(${\it info}$;$e$) $\in$ Id)
\\[0ex]\& ($\forall$$e$:$E$. rcv?(${\it info}$;$e$) $\Rightarrow$ loc(${\it info}$;sender(${\it info}$;$e$)) $=$ source(link(${\it info}$;$e$)) $\in$ Id)
\\[0ex]\& (\=$\forall$$e$:$E$, ${\it e'}$:$E$.\+
\\[0ex]rcv?(${\it info}$;$e$)
\\[0ex]$\Rightarrow$ rcv?(${\it info}$;${\it e'}$)
\\[0ex]$\Rightarrow$ link(${\it info}$;$e$) $=$ link(${\it info}$;${\it e'}$) $\in$ IdLnk
\\[0ex]$\Rightarrow$ cless($E$;${\it pred?}$;${\it info}$;sender(${\it info}$;$e$);sender(${\it info}$;${\it e'}$))
\\[0ex]$\Rightarrow$ cless($E$;${\it pred?}$;${\it info}$;$e$;${\it e'}$))
\-\-
\end{tabbing}